YES 2.5300000000000002
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ CR
mainModule List
| ((sort :: [Bool] -> [Bool]) :: [Bool] -> [Bool]) |
module List where
| import qualified Maybe import qualified Prelude
|
| merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]
merge | cmp xs [] | = | xs |
merge | cmp [] ys | = | ys |
merge | cmp (x : xs) (y : ys) | = |
case | x `cmp` y of |
| GT | -> | y : merge cmp (x : xs) ys |
| _ | -> | x : merge cmp xs (y : ys) |
|
|
| merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]
merge_pairs | cmp [] | = | [] |
merge_pairs | cmp (xs : []) | = | xs : [] |
merge_pairs | cmp (xs : ys : xss) | = | merge cmp xs ys : merge_pairs cmp xss |
|
| mergesort :: (a -> a -> Ordering) -> [a] -> [a]
mergesort | cmp | = | mergesort' cmp . map wrap |
|
| mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]
mergesort' | cmp [] | = | [] |
mergesort' | cmp (xs : []) | = | xs |
mergesort' | cmp xss | = | mergesort' cmp (merge_pairs cmp xss) |
|
| sort :: Ord a => [a] -> [a]
sort | l | = | mergesort compare l |
|
| wrap :: a -> [a]
|
module Maybe where
| import qualified List import qualified Prelude
|
Case Reductions:
The following Case expression
case | cmp x y of |
| GT | → y : merge cmp (x : xs) ys |
| _ | → x : merge cmp xs (y : ys) |
is transformed to
merge0 | y cmp x xs ys GT | = y : merge cmp (x : xs) ys |
merge0 | y cmp x xs ys _ | = x : merge cmp xs (y : ys) |
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
mainModule List
| ((sort :: [Bool] -> [Bool]) :: [Bool] -> [Bool]) |
module List where
| import qualified Maybe import qualified Prelude
|
| merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]
merge | cmp xs [] | = | xs |
merge | cmp [] ys | = | ys |
merge | cmp (x : xs) (y : ys) | = | merge0 y cmp x xs ys (x `cmp` y) |
|
|
merge0 | y cmp x xs ys GT | = | y : merge cmp (x : xs) ys |
merge0 | y cmp x xs ys _ | = | x : merge cmp xs (y : ys) |
|
| merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]
merge_pairs | cmp [] | = | [] |
merge_pairs | cmp (xs : []) | = | xs : [] |
merge_pairs | cmp (xs : ys : xss) | = | merge cmp xs ys : merge_pairs cmp xss |
|
| mergesort :: (a -> a -> Ordering) -> [a] -> [a]
mergesort | cmp | = | mergesort' cmp . map wrap |
|
| mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]
mergesort' | cmp [] | = | [] |
mergesort' | cmp (xs : []) | = | xs |
mergesort' | cmp xss | = | mergesort' cmp (merge_pairs cmp xss) |
|
| sort :: Ord a => [a] -> [a]
sort | l | = | mergesort compare l |
|
| wrap :: a -> [a]
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((sort :: [Bool] -> [Bool]) :: [Bool] -> [Bool]) |
module List where
| import qualified Maybe import qualified Prelude
|
| merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]
merge | cmp xs [] | = | xs |
merge | cmp [] ys | = | ys |
merge | cmp (x : xs) (y : ys) | = | merge0 y cmp x xs ys (x `cmp` y) |
|
|
merge0 | y cmp x xs ys GT | = | y : merge cmp (x : xs) ys |
merge0 | y cmp x xs ys vw | = | x : merge cmp xs (y : ys) |
|
| merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]
merge_pairs | cmp [] | = | [] |
merge_pairs | cmp (xs : []) | = | xs : [] |
merge_pairs | cmp (xs : ys : xss) | = | merge cmp xs ys : merge_pairs cmp xss |
|
| mergesort :: (a -> a -> Ordering) -> [a] -> [a]
mergesort | cmp | = | mergesort' cmp . map wrap |
|
| mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]
mergesort' | cmp [] | = | [] |
mergesort' | cmp (xs : []) | = | xs |
mergesort' | cmp xss | = | mergesort' cmp (merge_pairs cmp xss) |
|
| sort :: Ord a => [a] -> [a]
sort | l | = | mergesort compare l |
|
| wrap :: a -> [a]
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
compare | x y |
| | x == y | |
| | x <= y | |
| | otherwise | |
|
is transformed to
compare | x y | = compare3 x y |
compare2 | x y True | = EQ |
compare2 | x y False | = compare1 x y (x <= y) |
compare1 | x y True | = LT |
compare1 | x y False | = compare0 x y otherwise |
compare3 | x y | = compare2 x y (x == y) |
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule List
| (sort :: [Bool] -> [Bool]) |
module List where
| import qualified Maybe import qualified Prelude
|
| merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]
merge | cmp xs [] | = | xs |
merge | cmp [] ys | = | ys |
merge | cmp (x : xs) (y : ys) | = | merge0 y cmp x xs ys (x `cmp` y) |
|
|
merge0 | y cmp x xs ys GT | = | y : merge cmp (x : xs) ys |
merge0 | y cmp x xs ys vw | = | x : merge cmp xs (y : ys) |
|
| merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]
merge_pairs | cmp [] | = | [] |
merge_pairs | cmp (xs : []) | = | xs : [] |
merge_pairs | cmp (xs : ys : xss) | = | merge cmp xs ys : merge_pairs cmp xss |
|
| mergesort :: (a -> a -> Ordering) -> [a] -> [a]
mergesort | cmp | = | mergesort' cmp . map wrap |
|
| mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]
mergesort' | cmp [] | = | [] |
mergesort' | cmp (xs : []) | = | xs |
mergesort' | cmp xss | = | mergesort' cmp (merge_pairs cmp xss) |
|
| sort :: Ord a => [a] -> [a]
sort | l | = | mergesort compare l |
|
| wrap :: a -> [a]
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_map(:(vz3110, vz3111)) → new_map(vz3111)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_map(:(vz3110, vz3111)) → new_map(vz3111)
The graph contains the following edges 1 > 1
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge0(vz44, vz45, vz46, vz47, GT, ba) → new_merge(:(vz45, vz46), vz47, ba)
new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(vz340, vz341), :(vz3500, vz3501), bb) → new_merge0(vz3500, vz340, vz341, vz3501, new_compare(vz340, vz3500, bb), bb)
new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba)
The TRS R consists of the following rules:
new_compare2(vz340, vz3500, bd) → error([])
new_compare(vz340, vz3500, ty_Int) → new_compare0(vz340, vz3500)
new_compare(vz340, vz3500, app(app(ty_Either, cc), cd)) → new_compare11(vz340, vz3500, cc, cd)
new_compare(vz340, vz3500, ty_Bool) → new_compare12(vz340, vz3500)
new_compare4(vz340, vz3500) → error([])
new_compare0(vz340, vz3500) → error([])
new_compare(vz340, vz3500, app(app(app(ty_@3, bf), bg), bh)) → new_compare9(vz340, vz3500, bf, bg, bh)
new_compare(vz340, vz3500, ty_Float) → new_compare6(vz340, vz3500)
new_compare(vz340, vz3500, ty_Char) → new_compare3(vz340, vz3500)
new_compare(vz340, vz3500, ty_@0) → new_compare4(vz340, vz3500)
new_compare12(True, False) → GT
new_compare(vz340, vz3500, app(app(ty_@2, ca), cb)) → new_compare10(vz340, vz3500, ca, cb)
new_compare7(vz340, vz3500) → error([])
new_compare12(True, True) → EQ
new_compare(vz340, vz3500, ty_Ordering) → new_compare13(vz340, vz3500)
new_compare9(vz340, vz3500, bf, bg, bh) → error([])
new_compare(vz340, vz3500, app(ty_Maybe, bc)) → new_compare1(vz340, vz3500, bc)
new_compare(vz340, vz3500, app(ty_Ratio, be)) → new_compare8(vz340, vz3500, be)
new_compare(vz340, vz3500, ty_Double) → new_compare5(vz340, vz3500)
new_compare6(vz340, vz3500) → error([])
new_compare8(vz340, vz3500, be) → error([])
new_compare(vz340, vz3500, app(ty_[], bd)) → new_compare2(vz340, vz3500, bd)
new_compare5(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_Integer) → new_compare7(vz340, vz3500)
new_compare11(vz340, vz3500, cc, cd) → error([])
new_compare3(vz340, vz3500) → error([])
new_compare10(vz340, vz3500, ca, cb) → error([])
new_compare12(False, False) → EQ
new_compare13(vz340, vz3500) → error([])
new_compare12(False, True) → LT
new_compare1(vz340, vz3500, bc) → error([])
The set Q consists of the following terms:
new_compare8(x0, x1, x2)
new_compare3(x0, x1)
new_compare(x0, x1, app(ty_[], x2))
new_compare12(True, True)
new_compare1(x0, x1, x2)
new_compare(x0, x1, ty_Int)
new_compare7(x0, x1)
new_compare4(x0, x1)
new_compare13(x0, x1)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare0(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare5(x0, x1)
new_compare(x0, x1, ty_Bool)
new_compare12(False, True)
new_compare12(True, False)
new_compare2(x0, x1, x2)
new_compare12(False, False)
new_compare(x0, x1, ty_Float)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Ordering)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare11(x0, x1, x2, x3)
new_compare9(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare10(x0, x1, x2, x3)
new_compare(x0, x1, ty_@0)
new_compare(x0, x1, ty_Integer)
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule new_merge(:(vz340, vz341), :(vz3500, vz3501), bb) → new_merge0(vz3500, vz340, vz341, vz3501, new_compare(vz340, vz3500, bb), bb) at position [4] we obtained the following new rules:
new_merge(:(x0, y1), :(x1, y3), ty_@0) → new_merge0(x1, x0, y1, y3, new_compare4(x0, x1), ty_@0)
new_merge(:(x0, y1), :(x1, y3), ty_Integer) → new_merge0(x1, x0, y1, y3, new_compare7(x0, x1), ty_Integer)
new_merge(:(x0, y1), :(x1, y3), app(app(app(ty_@3, x2), x3), x4)) → new_merge0(x1, x0, y1, y3, new_compare9(x0, x1, x2, x3, x4), app(app(app(ty_@3, x2), x3), x4))
new_merge(:(x0, y1), :(x1, y3), ty_Ordering) → new_merge0(x1, x0, y1, y3, new_compare13(x0, x1), ty_Ordering)
new_merge(:(x0, y1), :(x1, y3), ty_Int) → new_merge0(x1, x0, y1, y3, new_compare0(x0, x1), ty_Int)
new_merge(:(x0, y1), :(x1, y3), app(ty_Maybe, x2)) → new_merge0(x1, x0, y1, y3, new_compare1(x0, x1, x2), app(ty_Maybe, x2))
new_merge(:(x0, y1), :(x1, y3), app(ty_Ratio, x2)) → new_merge0(x1, x0, y1, y3, new_compare8(x0, x1, x2), app(ty_Ratio, x2))
new_merge(:(x0, y1), :(x1, y3), app(ty_[], x2)) → new_merge0(x1, x0, y1, y3, new_compare2(x0, x1, x2), app(ty_[], x2))
new_merge(:(x0, y1), :(x1, y3), ty_Bool) → new_merge0(x1, x0, y1, y3, new_compare12(x0, x1), ty_Bool)
new_merge(:(x0, y1), :(x1, y3), ty_Double) → new_merge0(x1, x0, y1, y3, new_compare5(x0, x1), ty_Double)
new_merge(:(x0, y1), :(x1, y3), app(app(ty_Either, x2), x3)) → new_merge0(x1, x0, y1, y3, new_compare11(x0, x1, x2, x3), app(app(ty_Either, x2), x3))
new_merge(:(x0, y1), :(x1, y3), app(app(ty_@2, x2), x3)) → new_merge0(x1, x0, y1, y3, new_compare10(x0, x1, x2, x3), app(app(ty_@2, x2), x3))
new_merge(:(x0, y1), :(x1, y3), ty_Float) → new_merge0(x1, x0, y1, y3, new_compare6(x0, x1), ty_Float)
new_merge(:(x0, y1), :(x1, y3), ty_Char) → new_merge0(x1, x0, y1, y3, new_compare3(x0, x1), ty_Char)
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge(:(x0, y1), :(x1, y3), ty_@0) → new_merge0(x1, x0, y1, y3, new_compare4(x0, x1), ty_@0)
new_merge(:(x0, y1), :(x1, y3), ty_Integer) → new_merge0(x1, x0, y1, y3, new_compare7(x0, x1), ty_Integer)
new_merge(:(x0, y1), :(x1, y3), app(app(app(ty_@3, x2), x3), x4)) → new_merge0(x1, x0, y1, y3, new_compare9(x0, x1, x2, x3, x4), app(app(app(ty_@3, x2), x3), x4))
new_merge0(vz44, vz45, vz46, vz47, GT, ba) → new_merge(:(vz45, vz46), vz47, ba)
new_merge(:(x0, y1), :(x1, y3), ty_Ordering) → new_merge0(x1, x0, y1, y3, new_compare13(x0, x1), ty_Ordering)
new_merge(:(x0, y1), :(x1, y3), ty_Int) → new_merge0(x1, x0, y1, y3, new_compare0(x0, x1), ty_Int)
new_merge(:(x0, y1), :(x1, y3), app(ty_Maybe, x2)) → new_merge0(x1, x0, y1, y3, new_compare1(x0, x1, x2), app(ty_Maybe, x2))
new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(x0, y1), :(x1, y3), app(ty_Ratio, x2)) → new_merge0(x1, x0, y1, y3, new_compare8(x0, x1, x2), app(ty_Ratio, x2))
new_merge(:(x0, y1), :(x1, y3), app(ty_[], x2)) → new_merge0(x1, x0, y1, y3, new_compare2(x0, x1, x2), app(ty_[], x2))
new_merge(:(x0, y1), :(x1, y3), ty_Bool) → new_merge0(x1, x0, y1, y3, new_compare12(x0, x1), ty_Bool)
new_merge(:(x0, y1), :(x1, y3), ty_Double) → new_merge0(x1, x0, y1, y3, new_compare5(x0, x1), ty_Double)
new_merge(:(x0, y1), :(x1, y3), app(app(ty_Either, x2), x3)) → new_merge0(x1, x0, y1, y3, new_compare11(x0, x1, x2, x3), app(app(ty_Either, x2), x3))
new_merge(:(x0, y1), :(x1, y3), app(app(ty_@2, x2), x3)) → new_merge0(x1, x0, y1, y3, new_compare10(x0, x1, x2, x3), app(app(ty_@2, x2), x3))
new_merge(:(x0, y1), :(x1, y3), ty_Float) → new_merge0(x1, x0, y1, y3, new_compare6(x0, x1), ty_Float)
new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(x0, y1), :(x1, y3), ty_Char) → new_merge0(x1, x0, y1, y3, new_compare3(x0, x1), ty_Char)
The TRS R consists of the following rules:
new_compare2(vz340, vz3500, bd) → error([])
new_compare(vz340, vz3500, ty_Int) → new_compare0(vz340, vz3500)
new_compare(vz340, vz3500, app(app(ty_Either, cc), cd)) → new_compare11(vz340, vz3500, cc, cd)
new_compare(vz340, vz3500, ty_Bool) → new_compare12(vz340, vz3500)
new_compare4(vz340, vz3500) → error([])
new_compare0(vz340, vz3500) → error([])
new_compare(vz340, vz3500, app(app(app(ty_@3, bf), bg), bh)) → new_compare9(vz340, vz3500, bf, bg, bh)
new_compare(vz340, vz3500, ty_Float) → new_compare6(vz340, vz3500)
new_compare(vz340, vz3500, ty_Char) → new_compare3(vz340, vz3500)
new_compare(vz340, vz3500, ty_@0) → new_compare4(vz340, vz3500)
new_compare12(True, False) → GT
new_compare(vz340, vz3500, app(app(ty_@2, ca), cb)) → new_compare10(vz340, vz3500, ca, cb)
new_compare7(vz340, vz3500) → error([])
new_compare12(True, True) → EQ
new_compare(vz340, vz3500, ty_Ordering) → new_compare13(vz340, vz3500)
new_compare9(vz340, vz3500, bf, bg, bh) → error([])
new_compare(vz340, vz3500, app(ty_Maybe, bc)) → new_compare1(vz340, vz3500, bc)
new_compare(vz340, vz3500, app(ty_Ratio, be)) → new_compare8(vz340, vz3500, be)
new_compare(vz340, vz3500, ty_Double) → new_compare5(vz340, vz3500)
new_compare6(vz340, vz3500) → error([])
new_compare8(vz340, vz3500, be) → error([])
new_compare(vz340, vz3500, app(ty_[], bd)) → new_compare2(vz340, vz3500, bd)
new_compare5(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_Integer) → new_compare7(vz340, vz3500)
new_compare11(vz340, vz3500, cc, cd) → error([])
new_compare3(vz340, vz3500) → error([])
new_compare10(vz340, vz3500, ca, cb) → error([])
new_compare12(False, False) → EQ
new_compare13(vz340, vz3500) → error([])
new_compare12(False, True) → LT
new_compare1(vz340, vz3500, bc) → error([])
The set Q consists of the following terms:
new_compare8(x0, x1, x2)
new_compare3(x0, x1)
new_compare(x0, x1, app(ty_[], x2))
new_compare12(True, True)
new_compare1(x0, x1, x2)
new_compare(x0, x1, ty_Int)
new_compare7(x0, x1)
new_compare4(x0, x1)
new_compare13(x0, x1)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare0(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare5(x0, x1)
new_compare(x0, x1, ty_Bool)
new_compare12(False, True)
new_compare12(True, False)
new_compare2(x0, x1, x2)
new_compare12(False, False)
new_compare(x0, x1, ty_Float)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Ordering)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare11(x0, x1, x2, x3)
new_compare9(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare10(x0, x1, x2, x3)
new_compare(x0, x1, ty_@0)
new_compare(x0, x1, ty_Integer)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 13 less nodes.
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge0(vz44, vz45, vz46, vz47, GT, ba) → new_merge(:(vz45, vz46), vz47, ba)
new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(x0, y1), :(x1, y3), ty_Bool) → new_merge0(x1, x0, y1, y3, new_compare12(x0, x1), ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba)
The TRS R consists of the following rules:
new_compare2(vz340, vz3500, bd) → error([])
new_compare(vz340, vz3500, ty_Int) → new_compare0(vz340, vz3500)
new_compare(vz340, vz3500, app(app(ty_Either, cc), cd)) → new_compare11(vz340, vz3500, cc, cd)
new_compare(vz340, vz3500, ty_Bool) → new_compare12(vz340, vz3500)
new_compare4(vz340, vz3500) → error([])
new_compare0(vz340, vz3500) → error([])
new_compare(vz340, vz3500, app(app(app(ty_@3, bf), bg), bh)) → new_compare9(vz340, vz3500, bf, bg, bh)
new_compare(vz340, vz3500, ty_Float) → new_compare6(vz340, vz3500)
new_compare(vz340, vz3500, ty_Char) → new_compare3(vz340, vz3500)
new_compare(vz340, vz3500, ty_@0) → new_compare4(vz340, vz3500)
new_compare12(True, False) → GT
new_compare(vz340, vz3500, app(app(ty_@2, ca), cb)) → new_compare10(vz340, vz3500, ca, cb)
new_compare7(vz340, vz3500) → error([])
new_compare12(True, True) → EQ
new_compare(vz340, vz3500, ty_Ordering) → new_compare13(vz340, vz3500)
new_compare9(vz340, vz3500, bf, bg, bh) → error([])
new_compare(vz340, vz3500, app(ty_Maybe, bc)) → new_compare1(vz340, vz3500, bc)
new_compare(vz340, vz3500, app(ty_Ratio, be)) → new_compare8(vz340, vz3500, be)
new_compare(vz340, vz3500, ty_Double) → new_compare5(vz340, vz3500)
new_compare6(vz340, vz3500) → error([])
new_compare8(vz340, vz3500, be) → error([])
new_compare(vz340, vz3500, app(ty_[], bd)) → new_compare2(vz340, vz3500, bd)
new_compare5(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_Integer) → new_compare7(vz340, vz3500)
new_compare11(vz340, vz3500, cc, cd) → error([])
new_compare3(vz340, vz3500) → error([])
new_compare10(vz340, vz3500, ca, cb) → error([])
new_compare12(False, False) → EQ
new_compare13(vz340, vz3500) → error([])
new_compare12(False, True) → LT
new_compare1(vz340, vz3500, bc) → error([])
The set Q consists of the following terms:
new_compare8(x0, x1, x2)
new_compare3(x0, x1)
new_compare(x0, x1, app(ty_[], x2))
new_compare12(True, True)
new_compare1(x0, x1, x2)
new_compare(x0, x1, ty_Int)
new_compare7(x0, x1)
new_compare4(x0, x1)
new_compare13(x0, x1)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare0(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare5(x0, x1)
new_compare(x0, x1, ty_Bool)
new_compare12(False, True)
new_compare12(True, False)
new_compare2(x0, x1, x2)
new_compare12(False, False)
new_compare(x0, x1, ty_Float)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Ordering)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare11(x0, x1, x2, x3)
new_compare9(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare10(x0, x1, x2, x3)
new_compare(x0, x1, ty_@0)
new_compare(x0, x1, ty_Integer)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge0(vz44, vz45, vz46, vz47, GT, ba) → new_merge(:(vz45, vz46), vz47, ba)
new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(x0, y1), :(x1, y3), ty_Bool) → new_merge0(x1, x0, y1, y3, new_compare12(x0, x1), ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba)
The TRS R consists of the following rules:
new_compare12(True, False) → GT
new_compare12(True, True) → EQ
new_compare12(False, False) → EQ
new_compare12(False, True) → LT
The set Q consists of the following terms:
new_compare8(x0, x1, x2)
new_compare3(x0, x1)
new_compare(x0, x1, app(ty_[], x2))
new_compare12(True, True)
new_compare1(x0, x1, x2)
new_compare(x0, x1, ty_Int)
new_compare7(x0, x1)
new_compare4(x0, x1)
new_compare13(x0, x1)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare0(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare5(x0, x1)
new_compare(x0, x1, ty_Bool)
new_compare12(False, True)
new_compare12(True, False)
new_compare2(x0, x1, x2)
new_compare12(False, False)
new_compare(x0, x1, ty_Float)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Ordering)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare11(x0, x1, x2, x3)
new_compare9(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare10(x0, x1, x2, x3)
new_compare(x0, x1, ty_@0)
new_compare(x0, x1, ty_Integer)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_compare8(x0, x1, x2)
new_compare3(x0, x1)
new_compare(x0, x1, app(ty_[], x2))
new_compare1(x0, x1, x2)
new_compare(x0, x1, ty_Int)
new_compare7(x0, x1)
new_compare4(x0, x1)
new_compare13(x0, x1)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare0(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare5(x0, x1)
new_compare(x0, x1, ty_Bool)
new_compare2(x0, x1, x2)
new_compare(x0, x1, ty_Float)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Ordering)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare11(x0, x1, x2, x3)
new_compare9(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare10(x0, x1, x2, x3)
new_compare(x0, x1, ty_@0)
new_compare(x0, x1, ty_Integer)
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge0(vz44, vz45, vz46, vz47, GT, ba) → new_merge(:(vz45, vz46), vz47, ba)
new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(x0, y1), :(x1, y3), ty_Bool) → new_merge0(x1, x0, y1, y3, new_compare12(x0, x1), ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba)
The TRS R consists of the following rules:
new_compare12(True, False) → GT
new_compare12(True, True) → EQ
new_compare12(False, False) → EQ
new_compare12(False, True) → LT
The set Q consists of the following terms:
new_compare12(True, True)
new_compare12(False, True)
new_compare12(True, False)
new_compare12(False, False)
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule new_merge(:(x0, y1), :(x1, y3), ty_Bool) → new_merge0(x1, x0, y1, y3, new_compare12(x0, x1), ty_Bool) at position [4] we obtained the following new rules:
new_merge(:(True, y1), :(True, y3), ty_Bool) → new_merge0(True, True, y1, y3, EQ, ty_Bool)
new_merge(:(False, y1), :(True, y3), ty_Bool) → new_merge0(True, False, y1, y3, LT, ty_Bool)
new_merge(:(False, y1), :(False, y3), ty_Bool) → new_merge0(False, False, y1, y3, EQ, ty_Bool)
new_merge(:(True, y1), :(False, y3), ty_Bool) → new_merge0(False, True, y1, y3, GT, ty_Bool)
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge0(vz44, vz45, vz46, vz47, GT, ba) → new_merge(:(vz45, vz46), vz47, ba)
new_merge(:(False, y1), :(False, y3), ty_Bool) → new_merge0(False, False, y1, y3, EQ, ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(True, y1), :(True, y3), ty_Bool) → new_merge0(True, True, y1, y3, EQ, ty_Bool)
new_merge(:(False, y1), :(True, y3), ty_Bool) → new_merge0(True, False, y1, y3, LT, ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(True, y1), :(False, y3), ty_Bool) → new_merge0(False, True, y1, y3, GT, ty_Bool)
The TRS R consists of the following rules:
new_compare12(True, False) → GT
new_compare12(True, True) → EQ
new_compare12(False, False) → EQ
new_compare12(False, True) → LT
The set Q consists of the following terms:
new_compare12(True, True)
new_compare12(False, True)
new_compare12(True, False)
new_compare12(False, False)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge0(vz44, vz45, vz46, vz47, GT, ba) → new_merge(:(vz45, vz46), vz47, ba)
new_merge(:(False, y1), :(False, y3), ty_Bool) → new_merge0(False, False, y1, y3, EQ, ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(True, y1), :(True, y3), ty_Bool) → new_merge0(True, True, y1, y3, EQ, ty_Bool)
new_merge(:(False, y1), :(True, y3), ty_Bool) → new_merge0(True, False, y1, y3, LT, ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(True, y1), :(False, y3), ty_Bool) → new_merge0(False, True, y1, y3, GT, ty_Bool)
R is empty.
The set Q consists of the following terms:
new_compare12(True, True)
new_compare12(False, True)
new_compare12(True, False)
new_compare12(False, False)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_compare12(True, True)
new_compare12(False, True)
new_compare12(True, False)
new_compare12(False, False)
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge0(vz44, vz45, vz46, vz47, GT, ba) → new_merge(:(vz45, vz46), vz47, ba)
new_merge(:(False, y1), :(False, y3), ty_Bool) → new_merge0(False, False, y1, y3, EQ, ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(True, y1), :(True, y3), ty_Bool) → new_merge0(True, True, y1, y3, EQ, ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(False, y1), :(True, y3), ty_Bool) → new_merge0(True, False, y1, y3, LT, ty_Bool)
new_merge(:(True, y1), :(False, y3), ty_Bool) → new_merge0(False, True, y1, y3, GT, ty_Bool)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule new_merge0(vz44, vz45, vz46, vz47, GT, ba) → new_merge(:(vz45, vz46), vz47, ba) we obtained the following new rules:
new_merge0(False, True, z0, z1, GT, ty_Bool) → new_merge(:(True, z0), z1, ty_Bool)
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge(:(False, y1), :(False, y3), ty_Bool) → new_merge0(False, False, y1, y3, EQ, ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(True, y1), :(True, y3), ty_Bool) → new_merge0(True, True, y1, y3, EQ, ty_Bool)
new_merge0(False, True, z0, z1, GT, ty_Bool) → new_merge(:(True, z0), z1, ty_Bool)
new_merge(:(False, y1), :(True, y3), ty_Bool) → new_merge0(True, False, y1, y3, LT, ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(True, y1), :(False, y3), ty_Bool) → new_merge0(False, True, y1, y3, GT, ty_Bool)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba) we obtained the following new rules:
new_merge0(False, False, z0, z1, EQ, ty_Bool) → new_merge(z0, :(False, z1), ty_Bool)
new_merge0(True, True, z0, z1, EQ, ty_Bool) → new_merge(z0, :(True, z1), ty_Bool)
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge(:(False, y1), :(False, y3), ty_Bool) → new_merge0(False, False, y1, y3, EQ, ty_Bool)
new_merge(:(True, y1), :(True, y3), ty_Bool) → new_merge0(True, True, y1, y3, EQ, ty_Bool)
new_merge0(False, False, z0, z1, EQ, ty_Bool) → new_merge(z0, :(False, z1), ty_Bool)
new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(False, y1), :(True, y3), ty_Bool) → new_merge0(True, False, y1, y3, LT, ty_Bool)
new_merge0(False, True, z0, z1, GT, ty_Bool) → new_merge(:(True, z0), z1, ty_Bool)
new_merge0(True, True, z0, z1, EQ, ty_Bool) → new_merge(z0, :(True, z1), ty_Bool)
new_merge(:(True, y1), :(False, y3), ty_Bool) → new_merge0(False, True, y1, y3, GT, ty_Bool)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba) we obtained the following new rules:
new_merge0(True, False, z0, z1, LT, ty_Bool) → new_merge(z0, :(True, z1), ty_Bool)
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge0(True, False, z0, z1, LT, ty_Bool) → new_merge(z0, :(True, z1), ty_Bool)
new_merge(:(False, y1), :(False, y3), ty_Bool) → new_merge0(False, False, y1, y3, EQ, ty_Bool)
new_merge(:(True, y1), :(True, y3), ty_Bool) → new_merge0(True, True, y1, y3, EQ, ty_Bool)
new_merge0(False, False, z0, z1, EQ, ty_Bool) → new_merge(z0, :(False, z1), ty_Bool)
new_merge0(False, True, z0, z1, GT, ty_Bool) → new_merge(:(True, z0), z1, ty_Bool)
new_merge(:(False, y1), :(True, y3), ty_Bool) → new_merge0(True, False, y1, y3, LT, ty_Bool)
new_merge(:(True, y1), :(False, y3), ty_Bool) → new_merge0(False, True, y1, y3, GT, ty_Bool)
new_merge0(True, True, z0, z1, EQ, ty_Bool) → new_merge(z0, :(True, z1), ty_Bool)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs.
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge0(True, False, z0, z1, LT, ty_Bool) → new_merge(z0, :(True, z1), ty_Bool)
new_merge(:(True, y1), :(True, y3), ty_Bool) → new_merge0(True, True, y1, y3, EQ, ty_Bool)
new_merge(:(False, y1), :(True, y3), ty_Bool) → new_merge0(True, False, y1, y3, LT, ty_Bool)
new_merge0(True, True, z0, z1, EQ, ty_Bool) → new_merge(z0, :(True, z1), ty_Bool)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_merge(:(True, y1), :(True, y3), ty_Bool) → new_merge0(True, True, y1, y3, EQ, ty_Bool)
The graph contains the following edges 1 > 1, 2 > 1, 1 > 2, 2 > 2, 1 > 3, 2 > 4, 3 >= 6
- new_merge(:(False, y1), :(True, y3), ty_Bool) → new_merge0(True, False, y1, y3, LT, ty_Bool)
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4, 3 >= 6
- new_merge0(True, True, z0, z1, EQ, ty_Bool) → new_merge(z0, :(True, z1), ty_Bool)
The graph contains the following edges 3 >= 1, 6 >= 3
- new_merge0(True, False, z0, z1, LT, ty_Bool) → new_merge(z0, :(True, z1), ty_Bool)
The graph contains the following edges 3 >= 1, 6 >= 3
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge0(False, True, z0, z1, GT, ty_Bool) → new_merge(:(True, z0), z1, ty_Bool)
new_merge(:(True, y1), :(False, y3), ty_Bool) → new_merge0(False, True, y1, y3, GT, ty_Bool)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_merge0(False, True, z0, z1, GT, ty_Bool) → new_merge(:(True, z0), z1, ty_Bool)
The graph contains the following edges 4 >= 2, 6 >= 3
- new_merge(:(True, y1), :(False, y3), ty_Bool) → new_merge0(False, True, y1, y3, GT, ty_Bool)
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4, 3 >= 6
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge(:(False, y1), :(False, y3), ty_Bool) → new_merge0(False, False, y1, y3, EQ, ty_Bool)
new_merge0(False, False, z0, z1, EQ, ty_Bool) → new_merge(z0, :(False, z1), ty_Bool)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_merge(:(False, y1), :(False, y3), ty_Bool) → new_merge0(False, False, y1, y3, EQ, ty_Bool)
The graph contains the following edges 1 > 1, 2 > 1, 1 > 2, 2 > 2, 1 > 3, 2 > 4, 3 >= 6
- new_merge0(False, False, z0, z1, EQ, ty_Bool) → new_merge(z0, :(False, z1), ty_Bool)
The graph contains the following edges 3 >= 1, 6 >= 3
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_merge_pairs(:(vz35110, :(vz351110, vz351111)), ba) → new_merge_pairs(vz351111, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_merge_pairs(:(vz35110, :(vz351110, vz351111)), ba) → new_merge_pairs(vz351111, ba)
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_mergesort'(vz34, :(vz350, []), ba) → new_mergesort'(new_merge2(vz34, vz350, ba), [], ba)
new_mergesort'(vz34, :(vz350, :(vz3510, vz3511)), ba) → new_mergesort'(new_merge1(vz34, vz350, vz3510, ba), new_merge_pairs0(vz3511, ba), ba)
The TRS R consists of the following rules:
new_compare2(vz340, vz3500, bd) → error([])
new_compare14(vz3500, vz35100, ty_Int) → new_compare0(vz3500, vz35100)
new_compare(vz340, vz3500, app(app(ty_Either, cc), cd)) → new_compare11(vz340, vz3500, cc, cd)
new_compare0(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_@0) → new_compare4(vz340, vz3500)
new_compare14(vz3500, vz35100, ty_Ordering) → new_compare13(vz3500, vz35100)
new_compare14(vz3500, vz35100, app(ty_Ratio, be)) → new_compare8(vz3500, vz35100, be)
new_merge00(vz44, vz45, vz46, vz47, LT, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare(vz340, vz3500, app(app(ty_@2, ca), cb)) → new_compare10(vz340, vz3500, ca, cb)
new_compare7(vz340, vz3500) → error([])
new_merge_pairs0(:(vz35110, :(vz351110, vz351111)), ba) → :(new_merge2(vz35110, vz351110, ba), new_merge_pairs0(vz351111, ba))
new_compare14(vz3500, vz35100, app(ty_[], bd)) → new_compare2(vz3500, vz35100, bd)
new_merge1(vz34, [], :(vz35100, vz35101), ba) → new_merge2(vz34, :(vz35100, vz35101), ba)
new_compare14(vz3500, vz35100, ty_@0) → new_compare4(vz3500, vz35100)
new_compare(vz340, vz3500, app(ty_Maybe, bc)) → new_compare1(vz340, vz3500, bc)
new_merge_pairs0(:(vz35110, []), ba) → :(vz35110, [])
new_compare14(vz3500, vz35100, app(ty_Maybe, bc)) → new_compare1(vz3500, vz35100, bc)
new_compare14(vz3500, vz35100, ty_Char) → new_compare3(vz3500, vz35100)
new_compare(vz340, vz3500, app(ty_Ratio, be)) → new_compare8(vz340, vz3500, be)
new_compare(vz340, vz3500, ty_Double) → new_compare5(vz340, vz3500)
new_merge1(vz34, :(vz3500, vz3501), :(vz35100, vz35101), ba) → new_merge2(vz34, new_merge00(vz35100, vz3500, vz3501, vz35101, new_compare14(vz3500, vz35100, ba), ba), ba)
new_compare(vz340, vz3500, app(ty_[], bd)) → new_compare2(vz340, vz3500, bd)
new_merge00(vz44, vz45, vz46, vz47, GT, bb) → :(vz44, new_merge2(:(vz45, vz46), vz47, bb))
new_compare(vz340, vz3500, ty_Integer) → new_compare7(vz340, vz3500)
new_compare3(vz340, vz3500) → error([])
new_compare11(vz340, vz3500, cc, cd) → error([])
new_compare14(vz3500, vz35100, app(app(ty_Either, cc), cd)) → new_compare11(vz3500, vz35100, cc, cd)
new_compare10(vz340, vz3500, ca, cb) → error([])
new_compare12(False, False) → EQ
new_merge2([], :(vz3500, vz3501), ba) → :(vz3500, vz3501)
new_compare14(vz3500, vz35100, ty_Bool) → new_compare12(vz3500, vz35100)
new_compare14(vz3500, vz35100, ty_Float) → new_compare6(vz3500, vz35100)
new_compare1(vz340, vz3500, bc) → error([])
new_compare(vz340, vz3500, ty_Int) → new_compare0(vz340, vz3500)
new_merge_pairs0([], ba) → []
new_compare(vz340, vz3500, ty_Bool) → new_compare12(vz340, vz3500)
new_compare4(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, app(app(ty_@2, ca), cb)) → new_compare10(vz3500, vz35100, ca, cb)
new_compare14(vz3500, vz35100, ty_Double) → new_compare5(vz3500, vz35100)
new_compare(vz340, vz3500, app(app(app(ty_@3, bf), bg), bh)) → new_compare9(vz340, vz3500, bf, bg, bh)
new_compare(vz340, vz3500, ty_Float) → new_compare6(vz340, vz3500)
new_compare(vz340, vz3500, ty_Char) → new_compare3(vz340, vz3500)
new_compare12(True, False) → GT
new_merge1(vz34, vz350, [], ba) → new_merge2(vz34, vz350, ba)
new_merge2(:(vz340, vz341), :(vz3500, vz3501), ba) → new_merge00(vz3500, vz340, vz341, vz3501, new_compare(vz340, vz3500, ba), ba)
new_compare12(True, True) → EQ
new_compare(vz340, vz3500, ty_Ordering) → new_compare13(vz340, vz3500)
new_compare9(vz340, vz3500, bf, bg, bh) → error([])
new_merge2(vz34, [], ba) → vz34
new_compare6(vz340, vz3500) → error([])
new_compare8(vz340, vz3500, be) → error([])
new_compare5(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, app(app(app(ty_@3, bf), bg), bh)) → new_compare9(vz3500, vz35100, bf, bg, bh)
new_compare14(vz3500, vz35100, ty_Integer) → new_compare7(vz3500, vz35100)
new_merge00(vz44, vz45, vz46, vz47, EQ, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare13(vz340, vz3500) → error([])
new_compare12(False, True) → LT
The set Q consists of the following terms:
new_compare8(x0, x1, x2)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_compare3(x0, x1)
new_compare7(x0, x1)
new_compare(x0, x1, ty_Int)
new_compare4(x0, x1)
new_compare13(x0, x1)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare(x0, x1, ty_Char)
new_compare5(x0, x1)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, ty_Bool)
new_compare2(x0, x1, x2)
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge2([], :(x0, x1), x2)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare12(False, False)
new_compare(x0, x1, ty_Float)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Ordering)
new_compare14(x0, x1, ty_Bool)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_merge1(x0, x1, [], x2)
new_compare14(x0, x1, ty_@0)
new_compare9(x0, x1, x2, x3, x4)
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, ty_@0)
new_compare(x0, x1, app(ty_[], x2))
new_compare12(True, True)
new_compare1(x0, x1, x2)
new_merge_pairs0([], x0)
new_compare14(x0, x1, ty_Char)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_compare0(x0, x1)
new_compare14(x0, x1, ty_Ordering)
new_compare14(x0, x1, app(ty_[], x2))
new_compare12(False, True)
new_compare12(True, False)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, ty_Integer)
new_compare14(x0, x1, ty_Int)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_compare14(x0, x1, ty_Float)
new_compare11(x0, x1, x2, x3)
new_merge_pairs0(:(x0, []), x1)
new_merge1(x0, [], :(x1, x2), x3)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, ty_Integer)
new_compare10(x0, x1, x2, x3)
new_compare14(x0, x1, ty_Double)
new_merge2(x0, [], x1)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
new_mergesort'(vz34, :(vz350, :(vz3510, vz3511)), ba) → new_mergesort'(new_merge1(vz34, vz350, vz3510, ba), new_merge_pairs0(vz3511, ba), ba)
The TRS R consists of the following rules:
new_compare2(vz340, vz3500, bd) → error([])
new_compare14(vz3500, vz35100, ty_Int) → new_compare0(vz3500, vz35100)
new_compare(vz340, vz3500, app(app(ty_Either, cc), cd)) → new_compare11(vz340, vz3500, cc, cd)
new_compare0(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_@0) → new_compare4(vz340, vz3500)
new_compare14(vz3500, vz35100, ty_Ordering) → new_compare13(vz3500, vz35100)
new_compare14(vz3500, vz35100, app(ty_Ratio, be)) → new_compare8(vz3500, vz35100, be)
new_merge00(vz44, vz45, vz46, vz47, LT, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare(vz340, vz3500, app(app(ty_@2, ca), cb)) → new_compare10(vz340, vz3500, ca, cb)
new_compare7(vz340, vz3500) → error([])
new_merge_pairs0(:(vz35110, :(vz351110, vz351111)), ba) → :(new_merge2(vz35110, vz351110, ba), new_merge_pairs0(vz351111, ba))
new_compare14(vz3500, vz35100, app(ty_[], bd)) → new_compare2(vz3500, vz35100, bd)
new_merge1(vz34, [], :(vz35100, vz35101), ba) → new_merge2(vz34, :(vz35100, vz35101), ba)
new_compare14(vz3500, vz35100, ty_@0) → new_compare4(vz3500, vz35100)
new_compare(vz340, vz3500, app(ty_Maybe, bc)) → new_compare1(vz340, vz3500, bc)
new_merge_pairs0(:(vz35110, []), ba) → :(vz35110, [])
new_compare14(vz3500, vz35100, app(ty_Maybe, bc)) → new_compare1(vz3500, vz35100, bc)
new_compare14(vz3500, vz35100, ty_Char) → new_compare3(vz3500, vz35100)
new_compare(vz340, vz3500, app(ty_Ratio, be)) → new_compare8(vz340, vz3500, be)
new_compare(vz340, vz3500, ty_Double) → new_compare5(vz340, vz3500)
new_merge1(vz34, :(vz3500, vz3501), :(vz35100, vz35101), ba) → new_merge2(vz34, new_merge00(vz35100, vz3500, vz3501, vz35101, new_compare14(vz3500, vz35100, ba), ba), ba)
new_compare(vz340, vz3500, app(ty_[], bd)) → new_compare2(vz340, vz3500, bd)
new_merge00(vz44, vz45, vz46, vz47, GT, bb) → :(vz44, new_merge2(:(vz45, vz46), vz47, bb))
new_compare(vz340, vz3500, ty_Integer) → new_compare7(vz340, vz3500)
new_compare3(vz340, vz3500) → error([])
new_compare11(vz340, vz3500, cc, cd) → error([])
new_compare14(vz3500, vz35100, app(app(ty_Either, cc), cd)) → new_compare11(vz3500, vz35100, cc, cd)
new_compare10(vz340, vz3500, ca, cb) → error([])
new_compare12(False, False) → EQ
new_merge2([], :(vz3500, vz3501), ba) → :(vz3500, vz3501)
new_compare14(vz3500, vz35100, ty_Bool) → new_compare12(vz3500, vz35100)
new_compare14(vz3500, vz35100, ty_Float) → new_compare6(vz3500, vz35100)
new_compare1(vz340, vz3500, bc) → error([])
new_compare(vz340, vz3500, ty_Int) → new_compare0(vz340, vz3500)
new_merge_pairs0([], ba) → []
new_compare(vz340, vz3500, ty_Bool) → new_compare12(vz340, vz3500)
new_compare4(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, app(app(ty_@2, ca), cb)) → new_compare10(vz3500, vz35100, ca, cb)
new_compare14(vz3500, vz35100, ty_Double) → new_compare5(vz3500, vz35100)
new_compare(vz340, vz3500, app(app(app(ty_@3, bf), bg), bh)) → new_compare9(vz340, vz3500, bf, bg, bh)
new_compare(vz340, vz3500, ty_Float) → new_compare6(vz340, vz3500)
new_compare(vz340, vz3500, ty_Char) → new_compare3(vz340, vz3500)
new_compare12(True, False) → GT
new_merge1(vz34, vz350, [], ba) → new_merge2(vz34, vz350, ba)
new_merge2(:(vz340, vz341), :(vz3500, vz3501), ba) → new_merge00(vz3500, vz340, vz341, vz3501, new_compare(vz340, vz3500, ba), ba)
new_compare12(True, True) → EQ
new_compare(vz340, vz3500, ty_Ordering) → new_compare13(vz340, vz3500)
new_compare9(vz340, vz3500, bf, bg, bh) → error([])
new_merge2(vz34, [], ba) → vz34
new_compare6(vz340, vz3500) → error([])
new_compare8(vz340, vz3500, be) → error([])
new_compare5(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, app(app(app(ty_@3, bf), bg), bh)) → new_compare9(vz3500, vz35100, bf, bg, bh)
new_compare14(vz3500, vz35100, ty_Integer) → new_compare7(vz3500, vz35100)
new_merge00(vz44, vz45, vz46, vz47, EQ, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare13(vz340, vz3500) → error([])
new_compare12(False, True) → LT
The set Q consists of the following terms:
new_compare8(x0, x1, x2)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_compare3(x0, x1)
new_compare7(x0, x1)
new_compare(x0, x1, ty_Int)
new_compare4(x0, x1)
new_compare13(x0, x1)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare(x0, x1, ty_Char)
new_compare5(x0, x1)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, ty_Bool)
new_compare2(x0, x1, x2)
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge2([], :(x0, x1), x2)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare12(False, False)
new_compare(x0, x1, ty_Float)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Ordering)
new_compare14(x0, x1, ty_Bool)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_merge1(x0, x1, [], x2)
new_compare14(x0, x1, ty_@0)
new_compare9(x0, x1, x2, x3, x4)
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, ty_@0)
new_compare(x0, x1, app(ty_[], x2))
new_compare12(True, True)
new_compare1(x0, x1, x2)
new_merge_pairs0([], x0)
new_compare14(x0, x1, ty_Char)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_compare0(x0, x1)
new_compare14(x0, x1, ty_Ordering)
new_compare14(x0, x1, app(ty_[], x2))
new_compare12(False, True)
new_compare12(True, False)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, ty_Integer)
new_compare14(x0, x1, ty_Int)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_compare14(x0, x1, ty_Float)
new_compare11(x0, x1, x2, x3)
new_merge_pairs0(:(x0, []), x1)
new_merge1(x0, [], :(x1, x2), x3)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, ty_Integer)
new_compare10(x0, x1, x2, x3)
new_compare14(x0, x1, ty_Double)
new_merge2(x0, [], x1)
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_mergesort'(vz34, :(vz350, :(vz3510, vz3511)), ba) → new_mergesort'(new_merge1(vz34, vz350, vz3510, ba), new_merge_pairs0(vz3511, ba), ba)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:
POL(:(x1, x2)) = 1 + x2
POL(EQ) = 1
POL(False) = 1
POL(GT) = 1
POL(LT) = 1
POL(True) = 1
POL([]) = 0
POL(app(x1, x2)) = 1 + x1 + x2
POL(error(x1)) = 0
POL(new_compare(x1, x2, x3)) = 1 + x1 + x2 + x3
POL(new_compare0(x1, x2)) = 1
POL(new_compare1(x1, x2, x3)) = 1
POL(new_compare10(x1, x2, x3, x4)) = 1
POL(new_compare11(x1, x2, x3, x4)) = 1
POL(new_compare12(x1, x2)) = 1 + x1
POL(new_compare13(x1, x2)) = 1 + x1
POL(new_compare14(x1, x2, x3)) = 0
POL(new_compare2(x1, x2, x3)) = 1
POL(new_compare3(x1, x2)) = 1
POL(new_compare4(x1, x2)) = 1
POL(new_compare5(x1, x2)) = 1
POL(new_compare6(x1, x2)) = 1 + x2
POL(new_compare7(x1, x2)) = 1
POL(new_compare8(x1, x2, x3)) = 1
POL(new_compare9(x1, x2, x3, x4, x5)) = 1
POL(new_merge00(x1, x2, x3, x4, x5, x6)) = 0
POL(new_merge1(x1, x2, x3, x4)) = 0
POL(new_merge2(x1, x2, x3)) = 0
POL(new_merge_pairs0(x1, x2)) = 1 + x1
POL(new_mergesort'(x1, x2, x3)) = x2
POL(ty_@0) = 1
POL(ty_@2) = 1
POL(ty_@3) = 0
POL(ty_Bool) = 1
POL(ty_Char) = 1
POL(ty_Double) = 1
POL(ty_Either) = 1
POL(ty_Float) = 1
POL(ty_Int) = 1
POL(ty_Integer) = 1
POL(ty_Maybe) = 0
POL(ty_Ordering) = 1
POL(ty_Ratio) = 0
POL(ty_[]) = 0
The following usable rules [17] were oriented:
new_merge_pairs0([], ba) → []
new_merge_pairs0(:(vz35110, []), ba) → :(vz35110, [])
new_merge_pairs0(:(vz35110, :(vz351110, vz351111)), ba) → :(new_merge2(vz35110, vz351110, ba), new_merge_pairs0(vz351111, ba))
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
Q DP problem:
P is empty.
The TRS R consists of the following rules:
new_compare2(vz340, vz3500, bd) → error([])
new_compare14(vz3500, vz35100, ty_Int) → new_compare0(vz3500, vz35100)
new_compare(vz340, vz3500, app(app(ty_Either, cc), cd)) → new_compare11(vz340, vz3500, cc, cd)
new_compare0(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_@0) → new_compare4(vz340, vz3500)
new_compare14(vz3500, vz35100, ty_Ordering) → new_compare13(vz3500, vz35100)
new_compare14(vz3500, vz35100, app(ty_Ratio, be)) → new_compare8(vz3500, vz35100, be)
new_merge00(vz44, vz45, vz46, vz47, LT, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare(vz340, vz3500, app(app(ty_@2, ca), cb)) → new_compare10(vz340, vz3500, ca, cb)
new_compare7(vz340, vz3500) → error([])
new_merge_pairs0(:(vz35110, :(vz351110, vz351111)), ba) → :(new_merge2(vz35110, vz351110, ba), new_merge_pairs0(vz351111, ba))
new_compare14(vz3500, vz35100, app(ty_[], bd)) → new_compare2(vz3500, vz35100, bd)
new_merge1(vz34, [], :(vz35100, vz35101), ba) → new_merge2(vz34, :(vz35100, vz35101), ba)
new_compare14(vz3500, vz35100, ty_@0) → new_compare4(vz3500, vz35100)
new_compare(vz340, vz3500, app(ty_Maybe, bc)) → new_compare1(vz340, vz3500, bc)
new_merge_pairs0(:(vz35110, []), ba) → :(vz35110, [])
new_compare14(vz3500, vz35100, app(ty_Maybe, bc)) → new_compare1(vz3500, vz35100, bc)
new_compare14(vz3500, vz35100, ty_Char) → new_compare3(vz3500, vz35100)
new_compare(vz340, vz3500, app(ty_Ratio, be)) → new_compare8(vz340, vz3500, be)
new_compare(vz340, vz3500, ty_Double) → new_compare5(vz340, vz3500)
new_merge1(vz34, :(vz3500, vz3501), :(vz35100, vz35101), ba) → new_merge2(vz34, new_merge00(vz35100, vz3500, vz3501, vz35101, new_compare14(vz3500, vz35100, ba), ba), ba)
new_compare(vz340, vz3500, app(ty_[], bd)) → new_compare2(vz340, vz3500, bd)
new_merge00(vz44, vz45, vz46, vz47, GT, bb) → :(vz44, new_merge2(:(vz45, vz46), vz47, bb))
new_compare(vz340, vz3500, ty_Integer) → new_compare7(vz340, vz3500)
new_compare3(vz340, vz3500) → error([])
new_compare11(vz340, vz3500, cc, cd) → error([])
new_compare14(vz3500, vz35100, app(app(ty_Either, cc), cd)) → new_compare11(vz3500, vz35100, cc, cd)
new_compare10(vz340, vz3500, ca, cb) → error([])
new_compare12(False, False) → EQ
new_merge2([], :(vz3500, vz3501), ba) → :(vz3500, vz3501)
new_compare14(vz3500, vz35100, ty_Bool) → new_compare12(vz3500, vz35100)
new_compare14(vz3500, vz35100, ty_Float) → new_compare6(vz3500, vz35100)
new_compare1(vz340, vz3500, bc) → error([])
new_compare(vz340, vz3500, ty_Int) → new_compare0(vz340, vz3500)
new_merge_pairs0([], ba) → []
new_compare(vz340, vz3500, ty_Bool) → new_compare12(vz340, vz3500)
new_compare4(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, app(app(ty_@2, ca), cb)) → new_compare10(vz3500, vz35100, ca, cb)
new_compare14(vz3500, vz35100, ty_Double) → new_compare5(vz3500, vz35100)
new_compare(vz340, vz3500, app(app(app(ty_@3, bf), bg), bh)) → new_compare9(vz340, vz3500, bf, bg, bh)
new_compare(vz340, vz3500, ty_Float) → new_compare6(vz340, vz3500)
new_compare(vz340, vz3500, ty_Char) → new_compare3(vz340, vz3500)
new_compare12(True, False) → GT
new_merge1(vz34, vz350, [], ba) → new_merge2(vz34, vz350, ba)
new_merge2(:(vz340, vz341), :(vz3500, vz3501), ba) → new_merge00(vz3500, vz340, vz341, vz3501, new_compare(vz340, vz3500, ba), ba)
new_compare12(True, True) → EQ
new_compare(vz340, vz3500, ty_Ordering) → new_compare13(vz340, vz3500)
new_compare9(vz340, vz3500, bf, bg, bh) → error([])
new_merge2(vz34, [], ba) → vz34
new_compare6(vz340, vz3500) → error([])
new_compare8(vz340, vz3500, be) → error([])
new_compare5(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, app(app(app(ty_@3, bf), bg), bh)) → new_compare9(vz3500, vz35100, bf, bg, bh)
new_compare14(vz3500, vz35100, ty_Integer) → new_compare7(vz3500, vz35100)
new_merge00(vz44, vz45, vz46, vz47, EQ, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare13(vz340, vz3500) → error([])
new_compare12(False, True) → LT
The set Q consists of the following terms:
new_compare8(x0, x1, x2)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_compare3(x0, x1)
new_compare7(x0, x1)
new_compare(x0, x1, ty_Int)
new_compare4(x0, x1)
new_compare13(x0, x1)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare(x0, x1, ty_Char)
new_compare5(x0, x1)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, ty_Bool)
new_compare2(x0, x1, x2)
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge2([], :(x0, x1), x2)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare12(False, False)
new_compare(x0, x1, ty_Float)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Ordering)
new_compare14(x0, x1, ty_Bool)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_merge1(x0, x1, [], x2)
new_compare14(x0, x1, ty_@0)
new_compare9(x0, x1, x2, x3, x4)
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, ty_@0)
new_compare(x0, x1, app(ty_[], x2))
new_compare12(True, True)
new_compare1(x0, x1, x2)
new_merge_pairs0([], x0)
new_compare14(x0, x1, ty_Char)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_compare0(x0, x1)
new_compare14(x0, x1, ty_Ordering)
new_compare14(x0, x1, app(ty_[], x2))
new_compare12(False, True)
new_compare12(True, False)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, ty_Integer)
new_compare14(x0, x1, ty_Int)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_compare14(x0, x1, ty_Float)
new_compare11(x0, x1, x2, x3)
new_merge_pairs0(:(x0, []), x1)
new_merge1(x0, [], :(x1, x2), x3)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, ty_Integer)
new_compare10(x0, x1, x2, x3)
new_compare14(x0, x1, ty_Double)
new_merge2(x0, [], x1)
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.